verification: state no-formal-proof stance + add registry data-integrity invariants - #21
Merged
Merged
Conversation
…ntegrity invariants gv-clade-index has no ABI/FFI surface, so there are no formal proofs to maintain here (the template Idris2 ABI proofs were removed earlier; see PROOF-NEEDS.md). Make that stance explicit and promote the registry's checkable invariants to executable "proofs". - verification/README.adoc + proofs/safety_case/traceability READMEs: document that formal proofs are N/A for this JS data/edge project and that correctness is assured by worker/test/ + the worker-ci gate; Idris2 proofs deferred until a native surface exists. - .machine_readable/6a2/STATE.a2ml: add [verification] section recording the stance. - worker/test/data.test.js: add invariants — prefixed == "<clade>-<name>", valid secondary codes, github primary-key uniqueness, uuid present/well-formed/unique (now 37 tests). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UCnxjXkN6uDj9YSANuGEgR
🔍 Hypatia Security ScanFindings: 67 issues detected
View findings[
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dependabot-automerge.yml",
"type": "missing_timeout_minutes",
"file": "dependabot-automerge.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in instant-sync.yml",
"type": "missing_timeout_minutes",
"file": "instant-sync.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
June 21, 2026 02:09
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
Follow-up to the "what proofs remain?" assessment for this repo. The conclusion: gv-clade-index has no outstanding formal proofs, and none are warranted — it's a
gv/dbJavaScript-Worker + VeriSimDB/KV registry with no native ABI/FFI surface to verify (the template Idris2 ABI proofs were deliberately removed earlier; seePROOF-NEEDS.md).This PR closes that out honestly: it makes the verification stance explicit (so audits/CRG don't expect theorem proofs here) and promotes the registry's real, checkable invariants to executable "proofs."
Changes
State the verification position —
verification/README.adoc(+proofs/,safety_case/,traceability/unit READMEs, previously one-line stubs):worker/test/) and theworker-cigate;STATE.a2mlgains a[verification]section recording the same.Executable invariants (the repo-appropriate "proofs") —
worker/test/data.test.jsnow also asserts:prefixed === "<clade>-<name>"for every repo (ADR-003);secondaryclade codes are valid and exclude the primary;githubslugs) are unique;uuids are present, well-formed, and unique;total_repos === |by_name| === Σ member_countand the 12-clade invariant.All verified against the live snapshot (203 repos): 0 violations.
Verified locally
37/37 tests pass (33 → 37) ·
eslintclean ·prettier --checkclean.Not changed
The contractile proof-integrity guardrails (
MUST/TRUST) and the documentedsrc/interface/*"no FFI surface" status are correct and left as-is.🤖 Generated with Claude Code
https://claude.ai/code/session_01UCnxjXkN6uDj9YSANuGEgR
Generated by Claude Code